(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #xee87e1554e3b5d2b) #x111000aaa1040204))
(constraint (= (f #x4d6b563e0249964d) #xd7bdfa4206dabad7))
(constraint (= (f #xec24e13ec4955baa) #x111910c01322a045))
(constraint (= (f #x4aee0e7b05e83053) #xb11111004a014ca8))
(constraint (= (f #x679903ed7a5616e2) #x98066c0000088811))
(constraint (= (f #xa01e61e8c0365c91) #xe022a239405ae5b3))
(constraint (= (f #x25ead6b54e9e6e6e) #xd8010000a1001111))
(constraint (= (f #xa65787e5303e46ee) #x518800008cc01911))
(constraint (= (f #x28015db35ee105ee) #xd57ea2048010ea01))
(constraint (= (f #x7c6b199d50eeed12) #x801046622a11102c))
(constraint (= (f #xd51e6da25e6b5cee) #x22a0100580100211))
(constraint (= (f #xa6418bae83de7373) #x519a644114000888))
(constraint (= (f #xbe3340b533e80e13) #x400c8b408c01710c))
(constraint (= (f #x870ba63ee418b6ae) #x7084418011a64011))
(constraint (= (f #xb7d26e3c72426b27) #x4000910008999048))
(constraint (= (f #x0cae20262ee9cc88) #x15f2606a733a5598))
(constraint (= (f #xb4dec69e4acdc1a0) #xdd634ba2df5642e0))
(constraint (= (f #x0415568da25b84c5) #x0c3ffb96e6ec8d4f))
(constraint (= (f #xea22e20b31264c5b) #x115d11d44cc99320))
(constraint (= (f #xde8687ee33cee656) #x201110010c011188))
(constraint (= (f #x1c5dea182d115648) #x24e63e287733fad8))
(constraint (= (f #x445998d28cce02a1) #xcceaa977955207e3))
(constraint (= (f #x1eead082ead17458) #x233f71873f739ce8))
(constraint (= (f #xe367d73e56473ed4) #x25a87942fac9437c))
(constraint (= (f #x881ca849206d325e) #x776215324d900c80))
(constraint (= (f #xe9651c617e5ea297) #x1008a21880001540))
(constraint (= (f #xeee3eb37035eb13d) #x33243d5905e3d347))
(constraint (= (f #x56e0bc6839ec5210) #xfb21c4b84a34f630))
(constraint (= (f #x13301b35230a4687) #xeccce4488cc51910))
(constraint (= (f #x94595c4ee8d99888) #xbcebe4d3396aa998))
(constraint (= (f #x7e49d2a8d0552c76) #x8012205522aa8108))
(constraint (= (f #xc59eec76644cb864) #x4ea3349aacd5c8ac))
(constraint (= (f #xd8433b8140eb4098) #x68c54c83c13dc1a8))
(constraint (= (f #xe5ed6a2d4a268db9) #x2e37be77de6b96cb))
(constraint (= (f #xabcc8bd4ca6038b9) #xfc559c7d5ea049cb))
(constraint (= (f #x5027a7eba217a2d3) #xaad8000045c80500))
(constraint (= (f #xae7a90a5845a84e4) #xf28fb1ee8cef8d2c))
(constraint (= (f #x8a9e4443ea21d259) #x9fa2ccc43e6276eb))
(constraint (= (f #x7adcc016ec4030d5) #x8f65403b34c0517f))
(constraint (= (f #xcc5cee76dcbb2634) #x54e5329b65cd6a5c))
(constraint (= (f #x7d941a002ee0217c) #x86bc2e0073206384))
(constraint (= (f #xbd3b8c01543d7017) #x4004433eaa8008e8))
(constraint (= (f #xa2844e1e9b4c812c) #xe78cd223add58374))
(constraint (= (f #xcc3e713618e5eb98) #x5442935a292e3ca8))
(constraint (= (f #x714238a8e950c2e2) #x88a9c455102a3111))
(constraint (= (f #xa7ec2e770e6e2806) #x5001110881111579))
(constraint (= (f #xdde9ee3154b3cd55) #x663a3253fdd457ff))
(constraint (= (f #x3400acac420a1220) #x5c01f5f4c61e3660))
(constraint (= (f #xba09b2d17a52ce39) #xce1ad7738ef7524b))
(constraint (= (f #x7d57404079e30357) #x80288bbb8000cc88))
(constraint (= (f #x35091bc478e28ca1) #x5f1b2c4c892795e3))
(constraint (= (f #x698b1a9e018e7e95) #xba9d2fa2029283bf))
(constraint (= (f #x692dbddaedc8ec01) #xbb76c66f36593403))
(constraint (= (f #x620ce7e5b333b76d) #xa615282ed554d9b7))
(constraint (= (f #x91b3a8367b69da82) #x6644454880002055))
(constraint (= (f #xd34a4187e1c12b9d) #x75dec28822437ca7))
(constraint (= (f #x544c693616bda76e) #xaab3104888000081))
(constraint (= (f #x7738e51b6b0e1cae) #x888410a400410211))
(constraint (= (f #x3908ab6455604389) #x4b19fdacffa0c49b))
(constraint (= (f #x60b2baade227e8c3) #x9944445001d80130))
(constraint (= (f #x31e9dcd76be7a705) #x523a6579bc28e90f))
(constraint (= (f #x7dd63673ad7d2514) #x867a5a94f7876f3c))
(constraint (= (f #x9868136acba1bdcc) #xa8b835bf5ce2c654))
(constraint (= (f #x48a11eb0745ab24c) #xd9e323d09cefd6d4))
(constraint (= (f #xaad06ad53144e59e) #x550291028cab1020))
(constraint (= (f #x773eb319208e8ec8) #x9943d52b61939358))
(constraint (= (f #x5c2ea80ab3b32de7) #xa21115754444c000))
(constraint (= (f #x2c1e74c3378b1d46) #xd1200830c8044229))
(constraint (= (f #xe5671091e4d6de50) #x2fa931b22d7b62f0))
(constraint (= (f #xb0111d32ee922cae) #x44eee20c1104d111))
(constraint (= (f #x700b92deceb153ee) #x88f444001104a801))
(constraint (= (f #x370d2382e066ed3c) #x5917648720ab3744))
(constraint (= (f #xe32d3171449a670b) #x10c00c88ab241884))
(constraint (= (f #x2eeac6ed9bc2ae5b) #xd111111024015100))
(constraint (= (f #xe84489699430b518) #x38cd9bbabc51df28))
(constraint (= (f #x599e162c8657cc63) #xa260089131880318))
(constraint (= (f #xe6d618ed2a23a7be) #x11008610055c4000))
(constraint (= (f #x17e760a9469b4e0b) #xe800895429040114))
(constraint (= (f #x9689c6ea3c006523) #x60162111403f988c))
(constraint (= (f #x59c665d83cd248cc) #xea4aae684576d954))
(constraint (= (f #x384db8c1cb0937e8) #x48d6c9425d1b5838))
(constraint (= (f #x4d2a2b8a4deea050) #xd77e7c9ed633e0f0))
(constraint (= (f #x813ee9529533eb78) #x83433bf7bf543d88))
(constraint (= (f #x40b5e5ec073c7395) #xc1de2e34094494bf))
(constraint (= (f #xa42cb6eee58625a1) #xec75db332e8a6ee3))
(constraint (= (f #x97e0e7dc61c10e6c) #xb8212864a24312b4))
(constraint (= (f #x04ed0bae2363445d) #x0d371cf265a5cce7))
(constraint (= (f #xee1d7d8325528976) #x11020024c8a85608))
(constraint (= (f #x8866a2c3034eca24) #x98abe74505d35e6c))
(constraint (= (f #x6ee57cbeb56bc1be) #x9110800000800240))
(constraint (= (f #x153e6ed86ab57ee4) #x3f42b368bfdf832c))
(constraint (= (f #xc02084e6d10091a4) #x40618d2b7301b2ec))
(constraint (= (f #x7403824e1eed18b8) #x9c0486d2233729c8))
(constraint (= (f #xe8e0e3a711aa6aee) #x111110408e451111))
(constraint (= (f #x75c20cc3e3ee7d07) #x8821d33000010028))
(constraint (= (f #x0dd2957b315d52ca) #xf22042804ca22811))
(constraint (= (f #x5a623b74be9ee022) #xa019c408000011dd))
(constraint (= (f #x6b49d9a03373ce38) #xbdda6ae055945248))
(constraint (= (f #x68acbeb78caa7459) #xb9f5c3d895fe9ceb))
(constraint (= (f #x8c198da5b343e3c5) #x942a96eed5c4244f))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvor #x0000000000000002 x) x) (bvnot (bvor (bvudiv x #x0000000000000010) x)) (bvxor (bvadd x x) x)))
